Nuprl Lemma : es-copies_wf 11,40
es:ES{i}, e:E, x:Id. e copies x  {i'} 
latex

DefinitionsTrue, T, A c B, i || a, P & Q, x:A. B(x), e copies x, , t  T, x:A. B(x)
Lemmases-E wf, es-loc-init, event system wf, true wf, squash wf, es-vartype wf, es-init wf, es-when wf, not wf, es-choose wf, unit wf, locl wf, nat wf, Id wf, es-send wf, es-Msg wf, es-state wf, es-trans wf, es state wf, es-kindtype wf, Knd wf, free-from-atom wf1

origin